es:event_system{i:l}, e:es-E(es), l:IdLnk, L:(es-E(es) List).
es-rcv-from(es; e; l; L)
 (i:int_seg(0; ||L||). 
 e':es-E(es)
 ((es-isrcv(es; e'))
  (es-lnk(es; e') = l)
  (es-sender(es; e') = e)
  (es-index(es; e') = i  ))) 

latex

Definitions	x:A. B(x), P  Q, x:A. B(x), P  Q, t  T, A c B, A  B, A, False, prop{i:l}, es-rcv-from(es; e; l; L), int_seg(i; j), P  Q, lelt(i; j; k)
Lemmas	es-rcv-from-member-index, select wf, length wf1, select member, assert wf, es-isrcv wf, es-lnk wf, es-sender wf, es-index wf, int seg wf, es-Msgl wf, es-sends wf, es-E wf, es-rcv-from wf, IdLnk wf, event system wf